Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    app(app(le,0),y)  → true
2:    app(app(le,app(s,x)),0)  → false
3:    app(app(le,app(s,x)),app(s,y))  → app(app(le,x),y)
4:    app(app(eq,0),0)  → true
5:    app(app(eq,0),app(s,y))  → false
6:    app(app(eq,app(s,x)),0)  → false
7:    app(app(eq,app(s,x)),app(s,y))  → app(app(eq,x),y)
8:    app(app(app(if,true),x),y)  → x
9:    app(app(app(if,false),x),y)  → y
10:    app(minsort,nil)  → nil
11:    app(minsort,app(app(cons,x),y))  → app(app(cons,app(app(min,x),y)),app(minsort,app(app(del,app(app(min,x),y)),app(app(cons,x),y))))
12:    app(app(min,x),nil)  → x
13:    app(app(min,x),app(app(cons,y),z))  → app(app(app(if,app(app(le,x),y)),app(app(min,x),z)),app(app(min,y),z))
14:    app(app(del,x),nil)  → nil
15:    app(app(del,x),app(app(cons,y),z))  → app(app(app(if,app(app(eq,x),y)),z),app(app(cons,y),app(app(del,x),z)))
There are 26 dependency pairs:
16:    APP(app(le,app(s,x)),app(s,y))  → APP(app(le,x),y)
17:    APP(app(le,app(s,x)),app(s,y))  → APP(le,x)
18:    APP(app(eq,app(s,x)),app(s,y))  → APP(app(eq,x),y)
19:    APP(app(eq,app(s,x)),app(s,y))  → APP(eq,x)
20:    APP(minsort,app(app(cons,x),y))  → APP(app(cons,app(app(min,x),y)),app(minsort,app(app(del,app(app(min,x),y)),app(app(cons,x),y))))
21:    APP(minsort,app(app(cons,x),y))  → APP(cons,app(app(min,x),y))
22:    APP(minsort,app(app(cons,x),y))  → APP(minsort,app(app(del,app(app(min,x),y)),app(app(cons,x),y)))
23:    APP(minsort,app(app(cons,x),y))  → APP(app(del,app(app(min,x),y)),app(app(cons,x),y))
24:    APP(minsort,app(app(cons,x),y))  → APP(del,app(app(min,x),y))
25:    APP(minsort,app(app(cons,x),y))  → APP(app(min,x),y)
26:    APP(minsort,app(app(cons,x),y))  → APP(min,x)
27:    APP(app(min,x),app(app(cons,y),z))  → APP(app(app(if,app(app(le,x),y)),app(app(min,x),z)),app(app(min,y),z))
28:    APP(app(min,x),app(app(cons,y),z))  → APP(app(if,app(app(le,x),y)),app(app(min,x),z))
29:    APP(app(min,x),app(app(cons,y),z))  → APP(if,app(app(le,x),y))
30:    APP(app(min,x),app(app(cons,y),z))  → APP(app(le,x),y)
31:    APP(app(min,x),app(app(cons,y),z))  → APP(le,x)
32:    APP(app(min,x),app(app(cons,y),z))  → APP(app(min,x),z)
33:    APP(app(min,x),app(app(cons,y),z))  → APP(app(min,y),z)
34:    APP(app(min,x),app(app(cons,y),z))  → APP(min,y)
35:    APP(app(del,x),app(app(cons,y),z))  → APP(app(app(if,app(app(eq,x),y)),z),app(app(cons,y),app(app(del,x),z)))
36:    APP(app(del,x),app(app(cons,y),z))  → APP(app(if,app(app(eq,x),y)),z)
37:    APP(app(del,x),app(app(cons,y),z))  → APP(if,app(app(eq,x),y))
38:    APP(app(del,x),app(app(cons,y),z))  → APP(app(eq,x),y)
39:    APP(app(del,x),app(app(cons,y),z))  → APP(eq,x)
40:    APP(app(del,x),app(app(cons,y),z))  → APP(app(cons,y),app(app(del,x),z))
41:    APP(app(del,x),app(app(cons,y),z))  → APP(app(del,x),z)
The approximated dependency graph contains one SCC: {16,18,20,22,23,25,27,28,30,32,33,35,36,38,41}.
Tyrolean Termination Tool  (1.23 seconds)   ---  May 3, 2006